googologywikiaorg-20200223-history
User blog:Emlightened/Extensions to the SK Calculus
Terms are identified up to equivalence ≡. A model is consistent iff K''' ≡ '''SK is false. *'S'''abc ≡ ac(bc) *'K'ab ≡ a *If ac ≡ bc, c is a free variable and c does not occur in a or b, a ≡ b Oracle-like Combinators The extensions additionally include some of the following terms. It is not guaranteed that all extensions or combinations of extensions are consistent. *'Q'ab ≡ '''K' if a≡b and Q'''ab ≡ '''SK otherwise *'E'''ab ≡ '''K' if there is some c such that ac ≡ b, and E'''ab ≡ '''SK otherwise *'C'''ab ≡ '''K'c for some c such that ac ≡ b (if it exists), and C'''ab ≡ '''SKK otherwise *'M'''abc ≡ '''K' if there is some d such that bd ≡ c and ad ≡ K', and '''M'abc ≡ '''SK otherwise *'N'''abc ≡ '''K'd for some d such that bd ≡ c and ad ≡ K', and '''N'abc ≡ '''SKK otherwise First off, K''' and '''SK represent the truth values true and false, respectively. Given this, it is somewhat clear what each of these does: *'Q' is a term which tests for equivalence, so Q'ab represents a≡b *'E is a term that represents an existential quantifier, so E'ab represents ∃c(ac≡b) *'C represents some choice function corresponding to E'. Multiple may satisfy the definition. *'M is a term that represents the image function, and corresponds to conditional existential quantification: M'abc represents ∃d(ad ''and bd ≡ c) *'''N represents some choice function corresponding to N'. Multiple may satisfy the definition. It is clear that some of these can be used to represent others. In particular: *'Q'''a ≡ '''E(K'a) *'E'ab ≡ ('Q(C'ab)'SKK)(SK)K''' *'''E ≡ M'('KK) *'C' ≡ N'('KK) *'M'''abc ≡ ('Q'('''N'abc)SKK)(SK)K''' ...Are Contradictory This has been provided mainly for interest purposes. '''SKQ is contradictory, see Wikipedia. SKN, however, may not be. I'll hopefully update this in a little bit with non-contradictory (incomplete) versions. I kinda forgot that SKQ was contradictory when writing... oops. Relatedly, the \(\Xi\) function uses the (almost definitely; it's very closely related to Q') contradictory combinator 'Ω. It says in the article that we are to just ignore the contradictory uses - but how? No such Ω''' satisfies the definition, whether we say it does or not. Presumably, it implies that '''Ω is not complete, despite the definition. Thoughts? Real-Valued Combinators: a Potential Fix? Let \(\mathbb S\) be the set of surreal numbers \(a\) with rank \(<\omega_1\) and value \(0 \leq a \leq 1\) (or maybe \(\mathbb S = \mathbb R\)...?). For \(a,b\in\mathbb S\), let \(a \vee b = \min\{a+b,1\}\), \(\lnot a = 1-a\), \(a\wedge b = \max\{a+b-1,0\}\), \(a\to b = \min\{1-a+b,1\}\) and \(\leftrightarrow = (a \to b) \wedge (b \to a)\). Then, we interpret \(\equiv\) as not a binary predicate, but instead a function \(\equiv:\Lambda \times \Lambda \to \mathbb S\), where \(\Lambda\) is the set of combinators. We also let K'i for each \(i \in \mathbb S\) be a combinator with ≡('K'iab,a) = i+(¬i*≡(a,b)) and ≡('K'iab,b) = ¬i+(i*≡(a,b)) be a ''real combination of the two combinators. You can probably see where this is going. Instead of using '''K and SK to represent truth values, we use the 'K'i, as here negation does have fixed points. Apologies for being incomplete. Category:Blog posts